digraph {
	"fake{(false R (!(A) | X((false R B))))}" [style=invisible]
	"{(false R (!(A) | X((false R B))))}" [root=true shape=doublecircle]
	"{(false R B), (false R (!(A) | X((false R B))))}" [shape=doublecircle]
	"{(false R false)}" [shape=doublecircle]
	"{}" [shape=doublecircle]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}"
	"{(false R B), (false R false), (true U true)}"
	"fake{(false R (!(A) | X((false R B))))}" -> "{(false R (!(A) | X((false R B))))}" [style=bold]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R B), (true U true), (false R (!(A) | X((false R B))))}" [label="{B, A}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R B), (false R false), (true U true)}" [label="{B, A}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R (!(A) | X((false R B))))}" [label="{C, B}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R false)}" [label="{C, B}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R B), (true U true), (false R (!(A) | X((false R B))))}" [label="{A}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R B), (false R false), (true U true)}" [label="{A}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R B), (true U true), (false R (!(A) | X((false R B))))}" [label="{C, A}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R B), (false R false), (true U true)}" [label="{C, A}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R B), (true U true), (false R (!(A) | X((false R B))))}" [label="{C, B, A}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R B), (false R false), (true U true)}" [label="{C, B, A}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R (!(A) | X((false R B))))}" [label="{}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R false)}" [label="{}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R (!(A) | X((false R B))))}" [label="{B}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R false)}" [label="{B}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R (!(A) | X((false R B))))}" [label="{C}"]
	"{(false R (!(A) | X((false R B))))}" -> "{(false R false)}" [label="{C}"]
	"{}" -> "{}" [label="{B, A}"]
	"{}" -> "{}" [label="{C, B}"]
	"{}" -> "{}" [label="{A}"]
	"{}" -> "{}" [label="{C, A}"]
	"{}" -> "{}" [label="{C, B, A}"]
	"{}" -> "{}" [label="{B}"]
	"{}" -> "{}" [label="{}"]
	"{}" -> "{}" [label="{C}"]
	"{(false R B), (false R (!(A) | X((false R B))))}" -> "{(false R B), (true U true), (false R (!(A) | X((false R B))))}" [label="{B, A}"]
	"{(false R B), (false R (!(A) | X((false R B))))}" -> "{(false R B), (false R false), (true U true)}" [label="{B, A}"]
	"{(false R B), (false R (!(A) | X((false R B))))}" -> "{(false R false)}" [label="{C, B}"]
	"{(false R B), (false R (!(A) | X((false R B))))}" -> "{(false R B), (false R (!(A) | X((false R B))))}" [label="{C, B}"]
	"{(false R B), (false R (!(A) | X((false R B))))}" -> "{(false R false)}" [label="{B}"]
	"{(false R B), (false R (!(A) | X((false R B))))}" -> "{(false R B), (false R (!(A) | X((false R B))))}" [label="{B}"]
	"{(false R B), (false R (!(A) | X((false R B))))}" -> "{(false R B), (true U true), (false R (!(A) | X((false R B))))}" [label="{C, B, A}"]
	"{(false R B), (false R (!(A) | X((false R B))))}" -> "{(false R B), (false R false), (true U true)}" [label="{C, B, A}"]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}" -> "{(false R B), (true U true), (false R (!(A) | X((false R B))))}" [label="{B, A}"]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}" -> "{(false R B), (false R false), (true U true)}" [label="{B, A}"]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}" -> "{(false R false)}" [label="{C, B}"]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}" -> "{(false R B), (false R (!(A) | X((false R B))))}" [label="{C, B}"]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}" -> "{(false R false)}" [label="{B}"]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}" -> "{(false R B), (false R (!(A) | X((false R B))))}" [label="{B}"]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}" -> "{(false R B), (true U true), (false R (!(A) | X((false R B))))}" [label="{C, B, A}"]
	"{(false R B), (true U true), (false R (!(A) | X((false R B))))}" -> "{(false R B), (false R false), (true U true)}" [label="{C, B, A}"]
	label="always implication next always
G (A -> X(G(B)) )"
	fontsize=20
}
